Fault Tree (FT) is a standard failure modeling technique that has beenextensively used to predict reliability, availability and safety of manycomplex engineering systems. In order to facilitate the formal analysis of FTbased analyses, a higher-order-logic formalization of FTs has been recentlyproposed. However, this formalization is quite limited in terms of handlinglarge systems and transformation of FT models into their correspondingReliability Block Diagram (RBD) structures, i.e., a frequently usedtransformation in reliability and availability analyses. In order to overcomethese limitations, we present a deep embedding based formalization of FTs. Inparticular, the paper presents a formalization of AND, OR and NOT FT gates,which are in turn used to formalize other commonly used FT gates, i.e., NAND,NOR, XOR, Inhibit, Comparator and majority Voting, and the formal verificationof their failure probability expressions. For illustration purposes, we presenta formal failure analysis of a communication gateway software for the nextgeneration air traffic management system.
展开▼
